package main;
import java.util.Arrays;
import java.util.Collection;
import java.util.Map;
import java.util.Vector;

public class Encoder {
	
	public static Vector<int[]> atLeastOne(int[] lits){
		int[] l = Arrays.copyOf(lits, lits.length);
		Vector<int[]> res = new Vector<int[]>();
		res.add(l);
		return res;
	}
	
	public static int[][] atMostOne(int[] lits){
		int dimension = lits.length;
		int[][] res = new int[(int) dimension*(dimension-1)/2][2];
		
		int counter = 0; 
		for (int i = 0; i < dimension; i++){
			for (int j = i+1; j < dimension; j++){
				int[] p = new int[2];
				p[0] = -lits[i];
				p[1] = -lits[j];
				res[counter++] = p;
			}
			
		}
		return res;
	}
	
	public static int[][] xor2(int s, int lit1, int lit2){
		int[][] cnf = new int[4][3];
		// CNF representing the "false" table of the expression lit1 <-> lit2 XOR lit3 
		cnf[0] = new int[]{-s, -lit1, -lit2}; 
		cnf[1] = new int[]{-s, lit1, lit2};
		cnf[2] = new int[]{s, -lit1, lit2};
		cnf[3] = new int[]{s, lit1, -lit2};
		return cnf;
	}
	
	
	
	public static int[][] xor3(int lit1, int lit2,int lit3, int s0){
		int[][] cnf = new int[8][4];	
		cnf[0] = new int[]{lit1,lit2,lit3,-s0};
		cnf[1] = new int[]{lit1,lit2,-lit3,s0};
		cnf[2] = new int[]{lit1,-lit2,lit3,s0};
		cnf[3] = new int[]{lit1,-lit2,-lit3,-s0};
		cnf[4] = new int[]{-lit1,lit2,lit3,s0};
		cnf[5] = new int[]{-lit1,lit2,-lit3,-s0};
		cnf[6] = new int[]{-lit1,-lit2,lit3,-s0};
		cnf[7] = new int[]{-lit1,-lit2,-lit3,s0};
		return cnf;
	}
	
	public static int[][] cOut(int lit1, int lit2,int lit3, int s1){
		int[][] cnf = new int[8][4];	
		cnf[0] = new int[]{-lit1,-lit2,-lit3,s1};
		cnf[1] = new int[]{-lit1,-lit2,lit3,s1};
		cnf[2] = new int[]{-lit1,lit2,-lit3,s1};
		cnf[3] = new int[]{-lit1,lit2,lit3,-s1};
		cnf[4] = new int[]{lit1,-lit2,-lit3,s1};
		cnf[5] = new int[]{lit1,-lit2,lit3,-s1};
		cnf[6] = new int[]{lit1,lit2,-lit3,-s1};
		cnf[7] = new int[]{lit1,lit2,lit3,-s1};
		return cnf;
	}
	
	public static int[] fullAdder(int[] lits, LiteralAlocatorAndMap map, Vector<int[]> cnf){
		int[] sumBinaryLits = null;
		int zeroLit = map.getZeroLit();
		if (lits.length <=3){
			// S1 = A xor B xor C
			// S2 = AB + C(A xor B)
			int s1 = map.newLiteral();
			int s2 = map.newLiteral();
			sumBinaryLits = new int[]{s1,s2};
			int[][] cnfAddition = xor3(lits[0],lits[1],lits.length<3?zeroLit:lits[2],s1);
			for (int[] is : cnfAddition) {
				cnf.add(is);
			}
			cnfAddition = cOut(lits[0],lits[1],lits.length<3?zeroLit:lits[2],s2);
			for (int[] clause : cnfAddition) {
				cnf.add(clause);
			}
		}
		else{
			int[] litsL = Arrays.copyOfRange(lits, 0, lits.length/2);
			int[] litsR = Arrays.copyOfRange(lits, lits.length/2, lits.length);
			int[] resL = fullAdder(litsL, map, cnf);
			int[] resR = fullAdder(litsR, map, cnf);
			int maxSize = Math.max(resL.length, resR.length);
			resL = padWithZero(zeroLit, resL, maxSize);
			resR = padWithZero(zeroLit, resR, maxSize);
			sumBinaryLits = sum2numbers(resL, resR, zeroLit, map, cnf);
			
		}
		return sumBinaryLits;
	}

	
	/**
	 * assuming the 2 numbers has the same number of bits
	 * @param resL
	 * @param resR
	 * @param cnf 
	 * @param map, 
	 * @return
	 */
	private static int[] sum2numbers(int[] resL, int[] resR, int zero, LiteralAlocatorAndMap map, Vector<int[]> cnf) {
		int c_in =zero; 
		int[] res = new int[resL.length+1];
		for (int i = 0; i < resR.length; i++) {
			int[] lits = {c_in,resL[i],resR[i]};
			int[] newLits = fullAdder(lits, map, cnf);
			c_in = newLits[1];
			res[i] = newLits[0];
		}
		res[res.length-1] = c_in;
		return res;
	}

	private static int[] padWithZero(int zero, int[] lits,
			int maxSize) {
		if (lits.length < maxSize){
			int oldLength = lits.length;
			lits = Arrays.copyOf(lits, maxSize);
			for (int i = oldLength; i < lits.length; i++) {
				lits[i] = zero;
				
			}
		}
		return lits;
	}

	public static Vector<int[]> atLeastOneFalse(int[] lits){
		int[] l = Arrays.copyOf(lits, lits.length);
		for (int i = 0; i < l.length; i++) {
			l[i] = -l[i];
		}
		return atLeastOne(l);
	}
	
	public static Vector<int[]> circles(LiteralAlocatorAndMap map){
		// No circles of size 4
		Vector<int[]> cnf = new Vector<int[]>();
		Map<Integer, Pair<Integer, Integer>> map2 = map.getLiteralsToEdgesMap();
		int[] edgeLits = map.getEdgeLiterals();
		
		for (int a=0; a<edgeLits.length; a++){
			for (int b=a+1; b<edgeLits.length; b++){
				for (int c=b+1; c<edgeLits.length; c++){
					for (int d=c+1; d<edgeLits.length; d++){
						Pair<Integer, Integer>[] edges = new Pair[]{map2.get(edgeLits[a]),map2.get(edgeLits[b]), map2.get(edgeLits[c]),map2.get(edgeLits[d])};
						if (Verifier.isCircle(edges, Arrays.asList(0,1,2,3))){
							int[] lits = new int[]{edgeLits[a], edgeLits[b], edgeLits[c], edgeLits[d]};
							cnf.addAll(atLeastOneFalse(lits));
						}
					}
				}
			}
		}
		
		for (int a=0; a<edgeLits.length; a++){
			for (int b=a+1; b<edgeLits.length; b++){
				for (int c=b+1; c<edgeLits.length; c++){
					Pair<Integer, Integer>[] edges = new Pair[]{map2.get(edgeLits[a]),map2.get(edgeLits[b]), map2.get(edgeLits[c])};
					if (Verifier.isCircle(edges, Arrays.asList(0,1,2))){
						int[] lits = new int[]{edgeLits[a], edgeLits[b], edgeLits[c]};
						cnf.addAll(atLeastOneFalse(lits));
					}
					
				}
			}
		}
		
		return cnf;
	}

	public static Collection<? extends int[]> optimizations(LiteralAlocatorAndMap map) {
		Vector<int[]> res = new Vector<>();
		int numOfVertices = map.getNumOfVertices();
		numOfVertices = numOfVertices%2==0?numOfVertices:numOfVertices-1;
		
		for (int i = 1; i <= numOfVertices; i+=2){
			int edgeLit = map.getEdgeLiteral(new Pair<Integer,Integer>(i,i+1));
			res.add(new int[]{edgeLit});
		}
		
//		// make sum of every line in the matrix 
//		numOfVertices = map.getNumOfVertices();
//		int logN = (int) (Math.log(numOfVertices)/Math.log(2));
//		int[][] rowSums = new int[numOfVertices][];
//		for (int i = 1; i <= numOfVertices; i++){
//			int[] sumBits = fullAdder(map.getRowLits(i), map, res);
//			rowSums[i-1] = sumBits;
//		}
//
//		//all line summeries greater then 0
//		for (int i = 0; i < rowSums.length; i++){
//			int cLast = map.newLiteral();
//			int x = rowSums[i][rowSums[i].length -1];
//			int[] clause = new int[]{x,cLast};
//			res.add(clause);
//			System.out.println(Arrays.toString(clause));
//			for (int j = rowSums[i].length - 2; j > 0 - 1; j--){
//				int cNew = map.newLiteral();
//				x = rowSums[i][j];
//				clause = new int[]{x,cNew,-cLast};
//				res.add(clause);
//				System.out.println(Arrays.toString(clause));
//				clause = new int[]{x,-cNew,cLast};
//				res.add(clause);
//				System.out.println(Arrays.toString(clause));
//				clause = new int[]{-x,cNew,cLast};
//				res.add(clause);
//				System.out.println(Arrays.toString(clause));
//				clause = new int[]{-x,-cNew,cLast};
//				res.add(clause);
//				System.out.println(Arrays.toString(clause));
//				cLast = cNew;
//			}
//			clause = new int[]{x,-cLast};
//			res.add(clause);
//			System.out.println(Arrays.toString(clause));
//			clause = new int[]{-x,cLast};
//			res.add(clause);
//			System.out.println(Arrays.toString(clause));
//		}
		
//		for (int i = 0; i < numOfVertices-1; i++){
//			//line i is greater or equals to line i+1
//			int cLast = map.newLiteral("c0" );
//			int x = rowSums[i][0];
//			int y = rowSums[i+1][0];
//			res.add(new int[]{x,y,cLast});
//			res.add(new int[]{x,-y,-cLast});
//			res.add(new int[]{-x,y,cLast});
//			res.add(new int[]{-x,-y,cLast});
//			
//			for (int j = 1; j < logN-1; j++){
//				int cNew = map.newLiteral("c" + j);
//				x = rowSums[i][j];
//				y = rowSums[i+1][j];
//				res.add(new int[]{x,y,cLast,-cNew});
//				res.add(new int[]{x,y,-cLast,cNew});
//				res.add(new int[]{x,-y,cLast,-cNew});
//				res.add(new int[]{x,-y,-cLast,-cNew});
//				res.add(new int[]{-x,y,cLast,cNew});
//				res.add(new int[]{-x,y,-cLast,cNew});
//				res.add(new int[]{-x,-y,cLast,-cNew});
//				res.add(new int[]{-x,-y,-cLast,cNew});
//				cLast = cNew;
//			}
//			res.add(new int[]{x,y,cLast});
//			res.add(new int[]{x,-y,cLast});
//			res.add(new int[]{x,-y,-cLast});
//			res.add(new int[]{-x,-y,cLast});
//			
//		}
//		
		
//		
//		int[][] newLiterals = new int[numOfVertices][logN];
//		for (int i = 0; i < numOfVertices-1; i++){
//			for (int j = 0; j < logN; j++){
//				newLiterals[i][j] = map.newLiteral();
//				int x = newLiterals[i][j];
//				int a = rowSums[i][j];
//				int b = rowSums[i+1][j];
//				int[][] clausesForLiteral = {{-x,-a,b},
//						{-x,a,-b},
//						{x,-a,-b},
//						{x,a,b}};
//				for (int c = 0; c<4; c++){
//					res.add(clausesForLiteral[c]);
//				}
//				
//			}
//		}
//		for (int i = 0; i < numOfVertices-1;i++){
//			for (int j = logN-1; j >= 0; j--){
//				int a = rowSums[i][j];
//				int b = rowSums[i+1][j];
//				int[] clause = new int[logN-j+1];
//				int clauseIndex = 0;
//				for (int k = j+1 ; k < logN-1 ; k++){
//					int x = newLiterals[i][k];
//					clause[clauseIndex++] = x;
//				}
//				clause[clauseIndex++] = a;
//				clause[clauseIndex++] = -b;
//						
//				res.add(clause);
//				
//			}
//		}
		return res;
	}
	
}
